/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package chameleon.model.NuGatManager.Strategy;

import chameleon.model.NuGatStructure.symbTable.SymbType;
import chameleon.model.NuGatStructure.symbTable.SymbLayer;
import chameleon.model.NuGatStructure.symbTable.SymbTable;
import chameleon.model.NuGatStructure.prop.PropGame;
import chameleon.model.NuGatStructure.utils.Node;
import chameleon.model.NuGatStructure.strategy.GameStrategy;
import chameleon.gameSolver.NuGat.NuGatInterface;
import chameleon.model.NuGatStructure.strategy.BuchiStrategy;
import chameleon.model.NuGatStructure.strategy.GenBuchiStrategy;
import chameleon.model.NuGatStructure.strategy.GenReactivityStrategy;
import chameleon.model.game.Game;
import com.sun.jna.Pointer;

/**
 *
 * @author simon
 */
public class GenReactivityBuchiGameStrategyComputation {
    private PropGame prop_;
    private NuGatInterface nugat_;
    private boolean construct_strategy_;
    private SymbLayer layer_;
    private Node var_;
    private Game game_;
    
    
    public GenReactivityBuchiGameStrategyComputation(PropGame prop_, boolean construct,
            Game game, NuGatInterface nugat) {
        this.prop_ = prop_;
        nugat_ = nugat;
        construct_strategy_ = construct;
        layer_ = new SymbLayer(Pointer.NULL, nugat);
        var_ = new Node(Pointer.NULL,nugat);
        game_ = game;
    }
    
    /**
     * This function comes from NuGaT source code gameCheckGenReactivityBuchiSpec.c
     */
    
    public GameStrategy checkGenReactivitySpec(){
        GenBuchiStrategy strategy = null;
        Node varList1 = new Node(Pointer.NULL,nugat_);
        Node varList2 = new Node(Pointer.NULL,nugat_);
        
        nugat_.Game_BeforeCheckingSpec(prop_.ptr());
        
        
        if (construct_strategy_){
            Node expr = new Node(prop_.getExprCore().ptr(),nugat_);

            expr = expr.cdr();
            game_declare_special_var(expr.llength());



            if (nugat_.get_text(nugat_.find_string(nugat_.PLAYER_NAME_1)).equals(
                    prop_.getPlayer())) {
                varList1 = varList1.cons(var_, new Node(Pointer.NULL,nugat_));
            }
            else {
                varList2 = varList2.cons(var_,new Node(Pointer.NULL,nugat_));
            }

            //Here the game bdd fsm is stored in the object prop.

            strategy = new GenReactivityStrategy(nugat_.Chameleon_Game_CheckGenReactivitySpec(prop_.ptr(),var_.ptr(), 1),
                    prop_,varList1,varList2, layer_,nugat_);
            strategy.setIsSuccess(nugat_.GameStrategy_get_isSuccess(strategy.ptr())==1);
        }
        return strategy;
    }
    
    public GameStrategy checkBuchiGameSpec(){
        Node varList1 = new Node(Pointer.NULL,nugat_);
        Node varList2 = new Node(Pointer.NULL,nugat_);
        
        nugat_.Game_BeforeCheckingSpec(prop_.ptr());
        
        Node expr = new Node(prop_.getExprCore().ptr(),nugat_);
            
        expr = expr.car();
        game_declare_special_var(expr.llength());
        
        

        if (nugat_.get_text(nugat_.find_string(nugat_.PLAYER_NAME_1)).equals(
                prop_.getPlayer())) {
            varList1 = varList1.cons(var_, new Node(Pointer.NULL,nugat_));
        }
        else {
            varList2 = varList2.cons(var_,new Node(Pointer.NULL,nugat_));
        }
        
        GameStrategy strategy = new BuchiStrategy(nugat_.Chameleon_Game_CheckBuchiGameSpec(prop_.ptr(),var_.ptr(), 1),
                prop_,varList1,varList2,layer_,nugat_);
        return strategy;
    }
    
    private void game_declare_special_var(int guaranteeNumber){

          String name = "XJ";
          int i = 0;

          SymbLayer layer;
          Node var = new Node(Pointer.NULL,nugat_);
          Node values;
          SymbType symbolicType;
          
          
          /* Create a new temporal layer (with arbitrary name). */
          SymbTable symbTable = game_.getGlobalSymbTable();
          layer = symbTable.createLayer(null, /* a new name will be created */
                                         nugat_.SYMB_LAYER_POS_BOTTOM);
          
          /* Create a new var with arbitrary name. A var name should be a
             fresh one for every specification. Otherwise, there is a chance
             that some caching in type-checking or node-to-bdd may result in a
             problem.
          */
          /* Loop until a free name is found. */
          do {
                //sprintf(name+2, "_%d", ++i);
                ++i;
                name = "XJ_"+i;
                var = var.findNode(nugat_.ATOM, nugat_.find_string(name),
                        Pointer.NULL);
                var = var.findNode(nugat_.DOT, Pointer.NULL, var.ptr());
          } while (!layer.canDeclareVar(var));
          

          /* Create a list of values. */
          values = new Node(nugat_.CompileFlatten_expand_range(0, guaranteeNumber - 1),
                  nugat_);
          /* We don't declare constants here since there are just numbers. */
          symbolicType = new SymbType(nugat_.SYMB_TYPE_ENUM, values,nugat_);
          layer.declareStateVar(var, symbolicType);

          /* Commit the layer to all encodings. */
          symbTable.commitLayer(layer);

          var_ = var;
          layer_ = layer;

          /*if(opt_verbose_level_gt(OptsHandler_get_instance(), 0)) {
            fprintf(nusmv_stdout, "\n -- VAR %s : 0 .. %d;", name, guaranteeNumber - 1);
          }*/

          return;
    }
}
